Termination Proof Script

Consider the TRS R consisting of the rewrite rules


1:		terms(N)	→ cons(recip(sqr(N)),n__terms(s(N)))
2:		sqr(0)	→ 0
3:		sqr(s(X))	→ s(add(sqr(X),dbl(X)))
4:		dbl(0)	→ 0
5:		dbl(s(X))	→ s(s(dbl(X)))
6:		add(0,X)	→ X
7:		add(s(X),Y)	→ s(add(X,Y))
8:		first(0,X)	→ nil
9:		first(s(X),cons(Y,Z))	→ cons(Y,n__first(X,activate(Z)))
10:		terms(X)	→ n__terms(X)
11:		first(X1,X2)	→ n__first(X1,X2)
12:		activate(n__terms(X))	→ terms(X)
13:		activate(n__first(X1,X2))	→ first(X1,X2)
14:		activate(X)	→ X

There are 9 dependency pairs:


15:		TERMS(N)	→ SQR(N)
16:		SQR(s(X))	→ ADD(sqr(X),dbl(X))
17:		SQR(s(X))	→ SQR(X)
18:		SQR(s(X))	→ DBL(X)
19:		DBL(s(X))	→ DBL(X)
20:		ADD(s(X),Y)	→ ADD(X,Y)
21:		FIRST(s(X),cons(Y,Z))	→ ACTIVATE(Z)
22:		ACTIVATE(n__terms(X))	→ TERMS(X)
23:		ACTIVATE(n__first(X1,X2))	→ FIRST(X1,X2)

The approximated dependency graph contains 4 SCCs: {20}, {19}, {17} and {21,23}.

Consider the SCC {20}. There are no usable rules. By taking the AF π with π(ADD) = 1 together with the lexicographic path order with empty precedence, rule 20 is strictly decreasing.

Consider the SCC {19}. There are no usable rules. By taking the AF π with π(DBL) = 1 together with the lexicographic path order with empty precedence, rule 19 is strictly decreasing.

Consider the SCC {17}. There are no usable rules. By taking the AF π with π(SQR) = 1 together with the lexicographic path order with empty precedence, rule 17 is strictly decreasing.

Consider the SCC {21,23}. There are no usable rules. By taking the AF π with π(ACTIVATE) = 1, π(FIRST) = π(n__first) = 2 and π(cons) = [2] together with the lexicographic path order with empty precedence, rule 23 is weakly decreasing and rule 21 is strictly decreasing.

Hence the TRS is terminating.

Tyrolean Termination Tool (0.02 seconds) --- May 4, 2006